|
| 1: |
|
or(T,T) |
→ T |
| 2: |
|
or(F,T) |
→ T |
| 3: |
|
or(T,F) |
→ T |
| 4: |
|
or(F,F) |
→ F |
| 5: |
|
and(T,B) |
→ B |
| 6: |
|
and(B,T) |
→ B |
| 7: |
|
and(F,B) |
→ F |
| 8: |
|
and(B,F) |
→ F |
| 9: |
|
imp(T,B) |
→ B |
| 10: |
|
imp(F,B) |
→ T |
| 11: |
|
not(T) |
→ F |
| 12: |
|
not(F) |
→ T |
| 13: |
|
if(T,B1,B2) |
→ B1 |
| 14: |
|
if(F,B1,B2) |
→ B2 |
| 15: |
|
eq(T,T) |
→ T |
| 16: |
|
eq(F,F) |
→ T |
| 17: |
|
eq(T,F) |
→ F |
| 18: |
|
eq(F,T) |
→ F |
| 19: |
|
eqt(nil,undefined) |
→ F |
| 20: |
|
eqt(nil,pid(N2)) |
→ F |
| 21: |
|
eqt(nil,int(N2)) |
→ F |
| 22: |
|
eqt(nil,cons(H2,T2)) |
→ F |
| 23: |
|
eqt(nil,tuple(H2,T2)) |
→ F |
| 24: |
|
eqt(nil,tuplenil(H2)) |
→ F |
| 25: |
|
eqt(a,nil) |
→ F |
| 26: |
|
eqt(a,a) |
→ T |
| 27: |
|
eqt(a,excl) |
→ F |
| 28: |
|
eqt(a,false) |
→ F |
| 29: |
|
eqt(a,lock) |
→ F |
| 30: |
|
eqt(a,locker) |
→ F |
| 31: |
|
eqt(a,mcrlrecord) |
→ F |
| 32: |
|
eqt(a,ok) |
→ F |
| 33: |
|
eqt(a,pending) |
→ F |
| 34: |
|
eqt(a,release) |
→ F |
| 35: |
|
eqt(a,request) |
→ F |
| 36: |
|
eqt(a,resource) |
→ F |
| 37: |
|
eqt(a,tag) |
→ F |
| 38: |
|
eqt(a,true) |
→ F |
| 39: |
|
eqt(a,undefined) |
→ F |
| 40: |
|
eqt(a,pid(N2)) |
→ F |
| 41: |
|
eqt(a,int(N2)) |
→ F |
| 42: |
|
eqt(a,cons(H2,T2)) |
→ F |
| 43: |
|
eqt(a,tuple(H2,T2)) |
→ F |
| 44: |
|
eqt(a,tuplenil(H2)) |
→ F |
| 45: |
|
eqt(excl,nil) |
→ F |
| 46: |
|
eqt(excl,a) |
→ F |
| 47: |
|
eqt(excl,excl) |
→ T |
| 48: |
|
eqt(excl,false) |
→ F |
| 49: |
|
eqt(excl,lock) |
→ F |
| 50: |
|
eqt(excl,locker) |
→ F |
| 51: |
|
eqt(excl,mcrlrecord) |
→ F |
| 52: |
|
eqt(excl,ok) |
→ F |
| 53: |
|
eqt(excl,pending) |
→ F |
| 54: |
|
eqt(excl,release) |
→ F |
| 55: |
|
eqt(excl,request) |
→ F |
| 56: |
|
eqt(excl,resource) |
→ F |
| 57: |
|
eqt(excl,tag) |
→ F |
| 58: |
|
eqt(excl,true) |
→ F |
| 59: |
|
eqt(excl,undefined) |
→ F |
| 60: |
|
eqt(excl,pid(N2)) |
→ F |
| 61: |
|
eqt(excl,eqt(false,int(N2))) |
→ F |
| 62: |
|
eqt(false,cons(H2,T2)) |
→ F |
| 63: |
|
eqt(false,tuple(H2,T2)) |
→ F |
| 64: |
|
eqt(false,tuplenil(H2)) |
→ F |
| 65: |
|
eqt(lock,nil) |
→ F |
| 66: |
|
eqt(lock,a) |
→ F |
| 67: |
|
eqt(lock,excl) |
→ F |
| 68: |
|
eqt(lock,false) |
→ F |
| 69: |
|
eqt(lock,lock) |
→ T |
| 70: |
|
eqt(lock,locker) |
→ F |
| 71: |
|
eqt(lock,mcrlrecord) |
→ F |
| 72: |
|
eqt(lock,ok) |
→ F |
| 73: |
|
eqt(lock,pending) |
→ F |
| 74: |
|
eqt(lock,release) |
→ F |
| 75: |
|
eqt(lock,request) |
→ F |
| 76: |
|
eqt(lock,resource) |
→ F |
| 77: |
|
eqt(lock,tag) |
→ F |
| 78: |
|
eqt(lock,true) |
→ F |
| 79: |
|
eqt(lock,undefined) |
→ F |
| 80: |
|
eqt(lock,pid(N2)) |
→ F |
| 81: |
|
eqt(lock,int(N2)) |
→ F |
| 82: |
|
eqt(lock,cons(H2,T2)) |
→ F |
| 83: |
|
eqt(lock,tuple(H2,T2)) |
→ F |
| 84: |
|
eqt(lock,tuplenil(H2)) |
→ F |
| 85: |
|
eqt(locker,nil) |
→ F |
| 86: |
|
eqt(locker,a) |
→ F |
| 87: |
|
eqt(locker,excl) |
→ F |
| 88: |
|
eqt(locker,false) |
→ F |
| 89: |
|
eqt(locker,lock) |
→ F |
| 90: |
|
eqt(locker,locker) |
→ T |
| 91: |
|
eqt(locker,mcrlrecord) |
→ F |
| 92: |
|
eqt(locker,ok) |
→ F |
| 93: |
|
eqt(locker,pending) |
→ F |
| 94: |
|
eqt(locker,release) |
→ F |
| 95: |
|
eqt(locker,request) |
→ F |
| 96: |
|
eqt(locker,resource) |
→ F |
| 97: |
|
eqt(locker,tag) |
→ F |
| 98: |
|
eqt(locker,true) |
→ F |
| 99: |
|
eqt(locker,undefined) |
→ F |
| 100: |
|
eqt(locker,pid(N2)) |
→ F |
| 101: |
|
eqt(locker,int(N2)) |
→ F |
| 102: |
|
eqt(locker,cons(H2,T2)) |
→ F |
| 103: |
|
eqt(locker,tuple(H2,T2)) |
→ F |
| 104: |
|
eqt(locker,tuplenil(H2)) |
→ F |
| 105: |
|
eqt(mcrlrecord,nil) |
→ F |
| 106: |
|
eqt(mcrlrecord,a) |
→ F |
| 107: |
|
eqt(mcrlrecord,excl) |
→ F |
| 108: |
|
eqt(mcrlrecord,false) |
→ F |
| 109: |
|
eqt(mcrlrecord,lock) |
→ F |
| 110: |
|
eqt(mcrlrecord,locker) |
→ F |
| 111: |
|
eqt(mcrlrecord,mcrlrecord) |
→ T |
| 112: |
|
eqt(mcrlrecord,ok) |
→ F |
| 113: |
|
eqt(mcrlrecord,pending) |
→ F |
| 114: |
|
eqt(mcrlrecord,release) |
→ F |
| 115: |
|
eqt(mcrlrecord,request) |
→ F |
| 116: |
|
eqt(mcrlrecord,resource) |
→ F |
| 117: |
|
eqt(ok,resource) |
→ F |
| 118: |
|
eqt(ok,tag) |
→ F |
| 119: |
|
eqt(ok,true) |
→ F |
| 120: |
|
eqt(ok,undefined) |
→ F |
| 121: |
|
eqt(ok,pid(N2)) |
→ F |
| 122: |
|
eqt(ok,int(N2)) |
→ F |
| 123: |
|
eqt(ok,cons(H2,T2)) |
→ F |
| 124: |
|
eqt(ok,tuple(H2,T2)) |
→ F |
| 125: |
|
eqt(ok,tuplenil(H2)) |
→ F |
| 126: |
|
eqt(pending,nil) |
→ F |
| 127: |
|
eqt(pending,a) |
→ F |
| 128: |
|
eqt(pending,excl) |
→ F |
| 129: |
|
eqt(pending,false) |
→ F |
| 130: |
|
eqt(pending,lock) |
→ F |
| 131: |
|
eqt(pending,locker) |
→ F |
| 132: |
|
eqt(pending,mcrlrecord) |
→ F |
| 133: |
|
eqt(pending,ok) |
→ F |
| 134: |
|
eqt(pending,pending) |
→ T |
| 135: |
|
eqt(pending,release) |
→ F |
| 136: |
|
eqt(pending,request) |
→ F |
| 137: |
|
eqt(pending,resource) |
→ F |
| 138: |
|
eqt(pending,tag) |
→ F |
| 139: |
|
eqt(pending,true) |
→ F |
| 140: |
|
eqt(pending,undefined) |
→ F |
| 141: |
|
eqt(pending,pid(N2)) |
→ F |
| 142: |
|
eqt(pending,int(N2)) |
→ F |
| 143: |
|
eqt(pending,cons(H2,T2)) |
→ F |
| 144: |
|
eqt(pending,tuple(H2,T2)) |
→ F |
| 145: |
|
eqt(pending,tuplenil(H2)) |
→ F |
| 146: |
|
eqt(release,nil) |
→ F |
| 147: |
|
eqt(release,a) |
→ F |
| 148: |
|
eqt(release,excl) |
→ F |
| 149: |
|
eqt(release,false) |
→ F |
| 150: |
|
eqt(release,lock) |
→ F |
| 151: |
|
eqt(release,locker) |
→ F |
| 152: |
|
eqt(release,mcrlrecord) |
→ F |
| 153: |
|
eqt(release,ok) |
→ F |
| 154: |
|
eqt(request,mcrlrecord) |
→ F |
| 155: |
|
eqt(request,ok) |
→ F |
| 156: |
|
eqt(request,pending) |
→ F |
| 157: |
|
eqt(request,release) |
→ F |
| 158: |
|
eqt(request,request) |
→ T |
| 159: |
|
eqt(request,resource) |
→ F |
| 160: |
|
eqt(request,tag) |
→ F |
| 161: |
|
eqt(request,true) |
→ F |
| 162: |
|
eqt(request,undefined) |
→ F |
| 163: |
|
eqt(request,pid(N2)) |
→ F |
| 164: |
|
eqt(request,int(N2)) |
→ F |
| 165: |
|
eqt(request,cons(H2,T2)) |
→ F |
| 166: |
|
eqt(request,tuple(H2,T2)) |
→ F |
| 167: |
|
eqt(request,tuplenil(H2)) |
→ F |
| 168: |
|
eqt(resource,nil) |
→ F |
| 169: |
|
eqt(resource,a) |
→ F |
| 170: |
|
eqt(resource,excl) |
→ F |
| 171: |
|
eqt(resource,false) |
→ F |
| 172: |
|
eqt(resource,lock) |
→ F |
| 173: |
|
eqt(resource,locker) |
→ F |
| 174: |
|
eqt(resource,mcrlrecord) |
→ F |
| 175: |
|
eqt(resource,ok) |
→ F |
| 176: |
|
eqt(resource,pending) |
→ F |
| 177: |
|
eqt(resource,release) |
→ F |
| 178: |
|
eqt(resource,request) |
→ F |
| 179: |
|
eqt(resource,resource) |
→ T |
| 180: |
|
eqt(resource,tag) |
→ F |
| 181: |
|
eqt(resource,true) |
→ F |
| 182: |
|
eqt(resource,undefined) |
→ F |
| 183: |
|
eqt(resource,pid(N2)) |
→ F |
| 184: |
|
eqt(resource,int(N2)) |
→ F |
| 185: |
|
eqt(resource,cons(H2,T2)) |
→ F |
| 186: |
|
eqt(resource,tuple(H2,T2)) |
→ F |
| 187: |
|
eqt(resource,tuplenil(H2)) |
→ F |
| 188: |
|
eqt(tag,nil) |
→ F |
| 189: |
|
eqt(tag,a) |
→ F |
| 190: |
|
eqt(tag,excl) |
→ F |
| 191: |
|
eqt(tag,false) |
→ F |
| 192: |
|
eqt(tag,lock) |
→ F |
| 193: |
|
eqt(tag,locker) |
→ F |
| 194: |
|
eqt(tag,mcrlrecord) |
→ F |
| 195: |
|
eqt(tag,ok) |
→ F |
| 196: |
|
eqt(tag,pending) |
→ F |
| 197: |
|
eqt(tag,release) |
→ F |
| 198: |
|
eqt(tag,request) |
→ F |
| 199: |
|
eqt(tag,resource) |
→ F |
| 200: |
|
eqt(tag,tag) |
→ T |
| 201: |
|
eqt(tag,true) |
→ F |
| 202: |
|
eqt(tag,undefined) |
→ F |
| 203: |
|
eqt(tag,pid(N2)) |
→ F |
| 204: |
|
eqt(tag,int(N2)) |
→ F |
| 205: |
|
eqt(tag,cons(H2,T2)) |
→ F |
| 206: |
|
eqt(tag,tuple(H2,T2)) |
→ F |
| 207: |
|
eqt(tag,tuplenil(H2)) |
→ F |
| 208: |
|
eqt(true,nil) |
→ F |
| 209: |
|
eqt(true,a) |
→ F |
| 210: |
|
eqt(true,excl) |
→ F |
| 211: |
|
eqt(true,false) |
→ F |
| 212: |
|
eqt(true,lock) |
→ F |
| 213: |
|
eqt(true,locker) |
→ F |
| 214: |
|
eqt(true,mcrlrecord) |
→ F |
| 215: |
|
eqt(true,ok) |
→ F |
| 216: |
|
eqt(true,pending) |
→ F |
| 217: |
|
eqt(true,release) |
→ F |
| 218: |
|
eqt(true,request) |
→ F |
| 219: |
|
eqt(true,resource) |
→ F |
| 220: |
|
eqt(true,tag) |
→ F |
| 221: |
|
eqt(true,true) |
→ T |
| 222: |
|
eqt(true,undefined) |
→ F |
| 223: |
|
eqt(true,pid(N2)) |
→ F |
| 224: |
|
eqt(true,int(N2)) |
→ F |
| 225: |
|
eqt(true,cons(H2,T2)) |
→ F |
| 226: |
|
eqt(true,tuple(H2,T2)) |
→ F |
| 227: |
|
eqt(true,tuplenil(H2)) |
→ F |
| 228: |
|
eqt(undefined,nil) |
→ F |
| 229: |
|
eqt(undefined,a) |
→ F |
| 230: |
|
eqt(undefined,tuplenil(H2)) |
→ F |
| 231: |
|
eqt(pid(N1),nil) |
→ F |
| 232: |
|
eqt(pid(N1),a) |
→ F |
| 233: |
|
eqt(pid(N1),excl) |
→ F |
| 234: |
|
eqt(pid(N1),false) |
→ F |
| 235: |
|
eqt(pid(N1),lock) |
→ F |
| 236: |
|
eqt(pid(N1),locker) |
→ F |
| 237: |
|
eqt(pid(N1),mcrlrecord) |
→ F |
| 238: |
|
eqt(pid(N1),ok) |
→ F |
| 239: |
|
eqt(pid(N1),pending) |
→ F |
| 240: |
|
eqt(pid(N1),release) |
→ F |
| 241: |
|
eqt(pid(N1),request) |
→ F |
| 242: |
|
eqt(pid(N1),resource) |
→ F |
| 243: |
|
eqt(pid(N1),tag) |
→ F |
| 244: |
|
eqt(pid(N1),true) |
→ F |
| 245: |
|
eqt(pid(N1),undefined) |
→ F |
| 246: |
|
eqt(pid(N1),pid(N2)) |
→ eqt(N1,N2) |
| 247: |
|
eqt(pid(N1),int(N2)) |
→ F |
| 248: |
|
eqt(pid(N1),cons(H2,T2)) |
→ F |
| 249: |
|
eqt(pid(N1),tuple(H2,T2)) |
→ F |
| 250: |
|
eqt(pid(N1),tuplenil(H2)) |
→ F |
| 251: |
|
eqt(int(N1),nil) |
→ F |
| 252: |
|
eqt(int(N1),a) |
→ F |
| 253: |
|
eqt(int(N1),excl) |
→ F |
| 254: |
|
eqt(int(N1),false) |
→ F |
| 255: |
|
eqt(int(N1),lock) |
→ F |
| 256: |
|
eqt(int(N1),locker) |
→ F |
| 257: |
|
eqt(int(N1),mcrlrecord) |
→ F |
| 258: |
|
eqt(int(N1),ok) |
→ F |
| 259: |
|
eqt(int(N1),pending) |
→ F |
| 260: |
|
eqt(int(N1),release) |
→ F |
| 261: |
|
eqt(int(N1),request) |
→ F |
| 262: |
|
eqt(int(N1),resource) |
→ F |
| 263: |
|
eqt(int(N1),tag) |
→ F |
| 264: |
|
eqt(int(N1),true) |
→ F |
| 265: |
|
eqt(int(N1),undefined) |
→ F |
| 266: |
|
eqt(cons(H1,T1),resource) |
→ F |
| 267: |
|
eqt(cons(H1,T1),tag) |
→ F |
| 268: |
|
eqt(cons(H1,T1),true) |
→ F |
| 269: |
|
eqt(cons(H1,T1),undefined) |
→ F |
| 270: |
|
eqt(cons(H1,T1),pid(N2)) |
→ F |
| 271: |
|
eqt(cons(H1,T1),int(N2)) |
→ F |
| 272: |
|
eqt(cons(H1,T1),cons(H2,T2)) |
→ and(eqt(H1,H2),eqt(T1,T2)) |
| 273: |
|
eqt(cons(H1,T1),tuple(H2,T2)) |
→ F |
| 274: |
|
eqt(cons(H1,T1),tuplenil(H2)) |
→ F |
| 275: |
|
eqt(tuple(H1,T1),nil) |
→ F |
| 276: |
|
eqt(tuple(H1,T1),a) |
→ F |
| 277: |
|
eqt(tuple(H1,T1),excl) |
→ F |
| 278: |
|
eqt(tuple(H1,T1),false) |
→ F |
| 279: |
|
eqt(tuple(H1,T1),lock) |
→ F |
| 280: |
|
eqt(tuple(H1,T1),locker) |
→ F |
| 281: |
|
eqt(tuple(H1,T1),mcrlrecord) |
→ F |
| 282: |
|
eqt(tuple(H1,T1),ok) |
→ F |
| 283: |
|
eqt(tuple(H1,T1),pending) |
→ F |
| 284: |
|
eqt(tuple(H1,T1),release) |
→ F |
| 285: |
|
eqt(tuple(H1,T1),request) |
→ F |
| 286: |
|
eqt(tuple(H1,T1),resource) |
→ F |
| 287: |
|
eqt(tuple(H1,T1),tag) |
→ F |
| 288: |
|
eqt(tuple(H1,T1),true) |
→ F |
| 289: |
|
eqt(tuple(H1,T1),undefined) |
→ F |
| 290: |
|
eqt(tuple(H1,T1),pid(N2)) |
→ F |
| 291: |
|
eqt(tuple(H1,T1),int(N2)) |
→ F |
| 292: |
|
eqt(tuple(H1,T1),cons(H2,T2)) |
→ F |
| 293: |
|
eqt(tuple(H1,T1),tuple(H2,T2)) |
→ and(eqt(H1,H2),eqt(T1,T2)) |
| 294: |
|
eqt(tuple(H1,T1),tuplenil(H2)) |
→ F |
| 295: |
|
eqt(tuplenil(H1),nil) |
→ F |
| 296: |
|
eqt(tuplenil(H1),a) |
→ F |
| 297: |
|
eqt(tuplenil(H1),excl) |
→ F |
| 298: |
|
eqt(tuplenil(H1),false) |
→ F |
| 299: |
|
eqt(tuplenil(H1),lock) |
→ F |
| 300: |
|
eqt(tuplenil(H1),locker) |
→ F |
| 301: |
|
eqt(tuplenil(H1),mcrlrecord) |
→ F |
| 302: |
|
eqt(tuplenil(H1),ok) |
→ F |
| 303: |
|
eqt(tuplenil(H1),pending) |
→ F |
| 304: |
|
eqt(tuplenil(H1),release) |
→ F |
| 305: |
|
eqt(tuplenil(H1),request) |
→ F |
| 306: |
|
eqt(tuplenil(H1),resource) |
→ F |
| 307: |
|
eqt(tuplenil(H1),tag) |
→ F |
| 308: |
|
eqt(tuplenil(H1),true) |
→ F |
| 309: |
|
eqt(tuplenil(H1),undefined) |
→ F |
| 310: |
|
eqt(tuplenil(H1),pid(N2)) |
→ F |
| 311: |
|
eqt(tuplenil(H1),int(N2)) |
→ F |
| 312: |
|
eqt(tuplenil(H1),cons(H2,T2)) |
→ F |
| 313: |
|
eqt(tuplenil(H1),tuple(H2,T2)) |
→ F |
| 314: |
|
eqt(tuplenil(H1),tuplenil(H2)) |
→ eqt(H1,H2) |
| 315: |
|
element(int(s(0)),tuplenil(T1)) |
→ T1 |
| 316: |
|
element(int(s(0)),tuple(T1,T2)) |
→ T1 |
| 317: |
|
element(int(s(s(N1))),tuple(T1,T2)) |
→ element(int(s(N1)),T2) |
| 318: |
|
record_new(lock) |
→ tuple(mcrlrecord,tuple(lock,tuple(undefined,tuple(nil,tuplenil(nil))))) |
| 319: |
|
record_extract(tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(F2))))),lock,resource) |
→ tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(F2))))) |
| 320: |
|
record_update(tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(F2))))),lock,pending,NewF) |
→ tuple(mcrlrecord,tuple(lock,tuple(F0,tuple(F1,tuplenil(NewF))))) |
| 321: |
|
record_updates(Record,Name,nil) |
→ Record |
| 322: |
|
record_updates(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) |
→ record_updates(record_update(Record,Name,Field,NewF),Name,Fields) |
| 323: |
|
locker2_map_promote_pending(nil,Pending) |
→ nil |
| 324: |
|
locker2_map_promote_pending(cons(Lock,Locks),Pending) |
→ cons(locker2_promote_pending(Lock,Pending),locker2_map_promote_pending(Locks,Pending)) |
| 325: |
|
locker2_map_claim_lock(nil,Resources,Client) |
→ nil |
| 326: |
|
locker2_map_claim_lock(cons(Lock,Locks),Resources,Client) |
→ cons(locker2_claim_lock(Lock,Resources,Client),locker2_map_claim_lock(Locks,Resources,Client)) |
| 327: |
|
locker2_map_add_pending(nil,Resources,Client) |
→ nil |
| 328: |
|
locker2_promote_pending(Lock,Client) |
→ case0(Client,Lock,record_extract(Lock,lock,pending)) |
| 329: |
|
case0(Client,Lock,cons(Client,Pendings)) |
→ record_updates(Lock,lock,cons(tuple(excl,tuplenil(Client)),cons(tuple(pending,tuplenil(Pendings)),nil))) |
| 330: |
|
case0(Client,Lock,MCRLFree0) |
→ Lock |
| 331: |
|
locker2_remove_pending(Lock,Client) |
→ record_updates(Lock,lock,cons(tuple(pending,tuplenil(subtract(record_extract(Lock,lock,pending),cons(Client,nil)))),nil)) |
| 332: |
|
locker2_add_pending(Lock,Resources,Client) |
→ case1(Client,Resources,Lock,member(record_extract(Lock,lock,resource),Resources)) |
| 333: |
|
case1(Client,Resources,Lock,true) |
→ record_updates(Lock,lock,cons(tuple(pending,tuplenil(append(record_extract(Lock,lock,pending),cons(Client,nil)))),nil)) |
| 334: |
|
case1(Client,Resources,Lock,false) |
→ Lock |
| 335: |
|
locker2_release_lock(Lock,Client) |
→ case2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock,excl))) |
| 336: |
|
case2(Client,Lock,true) |
→ record_updates(Lock,lock,cons(tuple(excllock,excl),nil)) |
| 337: |
|
case4(Client,Lock,MCRLFree1) |
→ false |
| 338: |
|
locker2_obtainables(nil,Client) |
→ true |
| 339: |
|
locker2_obtainables(cons(Lock,Locks),Client) |
→ case5(Client,Locks,Lock,member(Client,record_extract(Lock,lock,pending))) |
| 340: |
|
case5(Client,Locks,Lock,true) |
→ andt(locker2_obtainable(Lock,Client),locker2_obtainables(Locks,Client)) |
| 341: |
|
case5(Client,Locks,Lock,false) |
→ locker2_obtainables(Locks,Client) |
| 342: |
|
locker2_check_available(Resource,nil) |
→ false |
| 343: |
|
locker2_check_available(Resource,cons(Lock,Locks)) |
→ case6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock,resource))) |
| 344: |
|
case6(Locks,Lock,Resource,true) |
→ andt(equal(record_extract(Lock,lock,excl),nil),equal(record_extract(Lock,lock,pending),nil)) |
| 345: |
|
case6(Locks,Lock,Resource,false) |
→ locker2_check_available(Resource,Locks) |
| 346: |
|
locker2_check_availables(nil,Locks) |
→ true |
| 347: |
|
locker2_check_availables(cons(Resource,Resources),Locks) |
→ andt(locker2_check_available(Resource,Locks),locker2_check_availables(Resources,Locks)) |
| 348: |
|
locker2_adduniq(nil,List) |
→ List |
| 349: |
|
append(cons(Head,Tail),List) |
→ cons(Head,append(Tail,List)) |
| 350: |
|
subtract(List,nil) |
→ List |
| 351: |
|
subtract(List,cons(Head,Tail)) |
→ subtract(delete(Head,List),Tail) |
| 352: |
|
delete(E,nil) |
→ nil |
| 353: |
|
delete(E,cons(Head,Tail)) |
→ case8(Tail,Head,E,equal(E,Head)) |
| 354: |
|
case8(Tail,Head,E,true) |
→ Tail |
| 355: |
|
case8(Tail,Head,E,false) |
→ cons(Head,delete(E,Tail)) |
| 356: |
|
gen_tag(Pid) |
→ tuple(Pid,tuplenil(tag)) |
| 357: |
|
gen_modtageq(Client1,Client2) |
→ equal(Client1,Client2) |
| 358: |
|
member(E,nil) |
→ false |
| 359: |
|
member(E,cons(Head,Tail)) |
→ case9(Tail,Head,E,equal(E,Head)) |
| 360: |
|
case9(Tail,Head,E,true) |
→ true |
| 361: |
|
case9(Tail,Head,E,false) |
→ member(E,Tail) |
| 362: |
|
eqs(empty,empty) |
→ T |
| 363: |
|
eqs(empty,stack(E2,S2)) |
→ F |
| 364: |
|
eqs(stack(E1,S1),empty) |
→ F |
| 365: |
|
eqs(stack(E1,S1),stack(E2,S2)) |
→ and(eqt(E1,E2),eqs(S1,S2)) |
| 366: |
|
pushs(E1,S1) |
→ stack(E1,S1) |
| 367: |
|
pops(stack(E1,S1)) |
→ S1 |
| 368: |
|
tops(stack(E1,S1)) |
→ E1 |
| 369: |
|
istops(E1,empty) |
→ F |
| 370: |
|
istops(E1,stack(E2,S1)) |
→ eqt(E1,E2) |
| 371: |
|
eqc(nocalls,nocalls) |
→ T |
| 372: |
|
eqc(nocalls,calls(E2,S2,CS2)) |
→ F |
| 373: |
|
eqc(calls(E1,S1,CS1),nocalls) |
→ F |
| 374: |
|
eqc(calls(E1,S1,CS1),calls(E2,S2,CS2)) |
→ and(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2))) |
| 375: |
|
push(E1,E2,nocalls) |
→ calls(E1,stack(E2,empty),nocalls) |
| 376: |
|
push(E1,E2,calls(E3,S1,CS1)) |
→ push1(E1,E2,E3,S1,CS1,eqt(E1,E3)) |
| 377: |
|
push1(E1,E2,E3,S1,CS1,T) |
→ calls(E3,pushs(E2,S1),CS1) |
|
There are 61 dependency pairs:
|
| 378: |
|
EQT(pid(N1),pid(N2)) |
→ EQT(N1,N2) |
| 379: |
|
EQT(cons(H1,T1),cons(H2,T2)) |
→ AND(eqt(H1,H2),eqt(T1,T2)) |
| 380: |
|
EQT(cons(H1,T1),cons(H2,T2)) |
→ EQT(H1,H2) |
| 381: |
|
EQT(cons(H1,T1),cons(H2,T2)) |
→ EQT(T1,T2) |
| 382: |
|
EQT(tuple(H1,T1),tuple(H2,T2)) |
→ AND(eqt(H1,H2),eqt(T1,T2)) |
| 383: |
|
EQT(tuple(H1,T1),tuple(H2,T2)) |
→ EQT(H1,H2) |
| 384: |
|
EQT(tuple(H1,T1),tuple(H2,T2)) |
→ EQT(T1,T2) |
| 385: |
|
EQT(tuplenil(H1),tuplenil(H2)) |
→ EQT(H1,H2) |
| 386: |
|
ELEMENT(int(s(s(N1))),tuple(T1,T2)) |
→ ELEMENT(int(s(N1)),T2) |
| 387: |
|
RECORD_UPDATES(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) |
→ RECORD_UPDATES(record_update(Record,Name,Field,NewF),Name,Fields) |
| 388: |
|
RECORD_UPDATES(Record,Name,cons(tuple(Field,tuplenil(NewF)),Fields)) |
→ RECORD_UPDATE(Record,Name,Field,NewF) |
| 389: |
|
LOCKER2_MAP_PROMOTE_PENDING(cons(Lock,Locks),Pending) |
→ LOCKER2_PROMOTE_PENDING(Lock,Pending) |
| 390: |
|
LOCKER2_MAP_PROMOTE_PENDING(cons(Lock,Locks),Pending) |
→ LOCKER2_MAP_PROMOTE_PENDING(Locks,Pending) |
| 391: |
|
LOCKER2_MAP_CLAIM_LOCK(cons(Lock,Locks),Resources,Client) |
→ LOCKER2_MAP_CLAIM_LOCK(Locks,Resources,Client) |
| 392: |
|
LOCKER2_PROMOTE_PENDING(Lock,Client) |
→ CASE0(Client,Lock,record_extract(Lock,lock,pending)) |
| 393: |
|
LOCKER2_PROMOTE_PENDING(Lock,Client) |
→ RECORD_EXTRACT(Lock,lock,pending) |
| 394: |
|
CASE0(Client,Lock,cons(Client,Pendings)) |
→ RECORD_UPDATES(Lock,lock,cons(tuple(excl,tuplenil(Client)),cons(tuple(pending,tuplenil(Pendings)),nil))) |
| 395: |
|
LOCKER2_REMOVE_PENDING(Lock,Client) |
→ RECORD_UPDATES(Lock,lock,cons(tuple(pending,tuplenil(subtract(record_extract(Lock,lock,pending),cons(Client,nil)))),nil)) |
| 396: |
|
LOCKER2_REMOVE_PENDING(Lock,Client) |
→ SUBTRACT(record_extract(Lock,lock,pending),cons(Client,nil)) |
| 397: |
|
LOCKER2_REMOVE_PENDING(Lock,Client) |
→ RECORD_EXTRACT(Lock,lock,pending) |
| 398: |
|
LOCKER2_ADD_PENDING(Lock,Resources,Client) |
→ CASE1(Client,Resources,Lock,member(record_extract(Lock,lock,resource),Resources)) |
| 399: |
|
LOCKER2_ADD_PENDING(Lock,Resources,Client) |
→ MEMBER(record_extract(Lock,lock,resource),Resources) |
| 400: |
|
LOCKER2_ADD_PENDING(Lock,Resources,Client) |
→ RECORD_EXTRACT(Lock,lock,resource) |
| 401: |
|
CASE1(Client,Resources,Lock,true) |
→ RECORD_UPDATES(Lock,lock,cons(tuple(pending,tuplenil(append(record_extract(Lock,lock,pending),cons(Client,nil)))),nil)) |
| 402: |
|
CASE1(Client,Resources,Lock,true) |
→ APPEND(record_extract(Lock,lock,pending),cons(Client,nil)) |
| 403: |
|
CASE1(Client,Resources,Lock,true) |
→ RECORD_EXTRACT(Lock,lock,pending) |
| 404: |
|
LOCKER2_RELEASE_LOCK(Lock,Client) |
→ CASE2(Client,Lock,gen_modtageq(Client,record_extract(Lock,lock,excl))) |
| 405: |
|
LOCKER2_RELEASE_LOCK(Lock,Client) |
→ GEN_MODTAGEQ(Client,record_extract(Lock,lock,excl)) |
| 406: |
|
LOCKER2_RELEASE_LOCK(Lock,Client) |
→ RECORD_EXTRACT(Lock,lock,excl) |
| 407: |
|
CASE2(Client,Lock,true) |
→ RECORD_UPDATES(Lock,lock,cons(tuple(excllock,excl),nil)) |
| 408: |
|
LOCKER2_OBTAINABLES(cons(Lock,Locks),Client) |
→ CASE5(Client,Locks,Lock,member(Client,record_extract(Lock,lock,pending))) |
| 409: |
|
LOCKER2_OBTAINABLES(cons(Lock,Locks),Client) |
→ MEMBER(Client,record_extract(Lock,lock,pending)) |
| 410: |
|
LOCKER2_OBTAINABLES(cons(Lock,Locks),Client) |
→ RECORD_EXTRACT(Lock,lock,pending) |
| 411: |
|
CASE5(Client,Locks,Lock,true) |
→ LOCKER2_OBTAINABLES(Locks,Client) |
| 412: |
|
CASE5(Client,Locks,Lock,false) |
→ LOCKER2_OBTAINABLES(Locks,Client) |
| 413: |
|
LOCKER2_CHECK_AVAILABLE(Resource,cons(Lock,Locks)) |
→ CASE6(Locks,Lock,Resource,equal(Resource,record_extract(Lock,lock,resource))) |
| 414: |
|
LOCKER2_CHECK_AVAILABLE(Resource,cons(Lock,Locks)) |
→ RECORD_EXTRACT(Lock,lock,resource) |
| 415: |
|
CASE6(Locks,Lock,Resource,true) |
→ RECORD_EXTRACT(Lock,lock,excl) |
| 416: |
|
CASE6(Locks,Lock,Resource,true) |
→ RECORD_EXTRACT(Lock,lock,pending) |
| 417: |
|
CASE6(Locks,Lock,Resource,false) |
→ LOCKER2_CHECK_AVAILABLE(Resource,Locks) |
| 418: |
|
LOCKER2_CHECK_AVAILABLES(cons(Resource,Resources),Locks) |
→ LOCKER2_CHECK_AVAILABLE(Resource,Locks) |
| 419: |
|
LOCKER2_CHECK_AVAILABLES(cons(Resource,Resources),Locks) |
→ LOCKER2_CHECK_AVAILABLES(Resources,Locks) |
| 420: |
|
APPEND(cons(Head,Tail),List) |
→ APPEND(Tail,List) |
| 421: |
|
SUBTRACT(List,cons(Head,Tail)) |
→ SUBTRACT(delete(Head,List),Tail) |
| 422: |
|
SUBTRACT(List,cons(Head,Tail)) |
→ DELETE(Head,List) |
| 423: |
|
DELETE(E,cons(Head,Tail)) |
→ CASE8(Tail,Head,E,equal(E,Head)) |
| 424: |
|
CASE8(Tail,Head,E,false) |
→ DELETE(E,Tail) |
| 425: |
|
MEMBER(E,cons(Head,Tail)) |
→ CASE9(Tail,Head,E,equal(E,Head)) |
| 426: |
|
CASE9(Tail,Head,E,false) |
→ MEMBER(E,Tail) |
| 427: |
|
EQS(stack(E1,S1),stack(E2,S2)) |
→ AND(eqt(E1,E2),eqs(S1,S2)) |
| 428: |
|
EQS(stack(E1,S1),stack(E2,S2)) |
→ EQT(E1,E2) |
| 429: |
|
EQS(stack(E1,S1),stack(E2,S2)) |
→ EQS(S1,S2) |
| 430: |
|
ISTOPS(E1,stack(E2,S1)) |
→ EQT(E1,E2) |
| 431: |
|
EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) |
→ AND(eqt(E1,E2),and(eqs(S1,S2),eqc(CS1,CS2))) |
| 432: |
|
EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) |
→ EQT(E1,E2) |
| 433: |
|
EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) |
→ AND(eqs(S1,S2),eqc(CS1,CS2)) |
| 434: |
|
EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) |
→ EQS(S1,S2) |
| 435: |
|
EQC(calls(E1,S1,CS1),calls(E2,S2,CS2)) |
→ EQC(CS1,CS2) |
| 436: |
|
PUSH(E1,E2,calls(E3,S1,CS1)) |
→ PUSH1(E1,E2,E3,S1,CS1,eqt(E1,E3)) |
| 437: |
|
PUSH(E1,E2,calls(E3,S1,CS1)) |
→ EQT(E1,E3) |
| 438: |
|
PUSH1(E1,E2,E3,S1,CS1,T) |
→ PUSHS(E2,S1) |
|
The approximated dependency graph contains 11 SCCs:
{420},
{386},
{391},
{387},
{419},
{421},
{408,411,412},
{378,380,381,383-385},
{429},
{435}
and {390}.